Skip to main content

Enumeration of Minimal Unsatisfiable Cores and Maximal Satisfying Subsets

This tutorial illustrates how to use Z3 for extracting all minimal unsatisfiable cores together with all maximal satisfying subsets.

Origin​

The algorithm that we describe next represents the essence of the core extraction procedure by Liffiton and Malik and independently by Previti and Marques-Silva:

Enumerating Infeasibility: Finding Multiple MUSes Quickly Mark H. Liffiton and Ammar Malik in Proc. 10th International Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) techniques in Constraint Programming (CPAIOR-2013), 160-175, May 2013.

Partial MUS Enumeration Alessandro Previti, Joao Marques-Silva in Proc. AAAI-2013 July 2013

Z3py Features​

This implementation contains no tuning. It was contributed by Mark Liffiton and it is a simplification of one of the versions available from his Marco Polo Web site. Code for eMUS is also [available. The example illustrates the following features of Z3's Python-based API:

  • Using assumptions to track unsatisfiable cores.
  • Using multiple solvers and passing constraints between them.
  • Calling the C-based API from Python. Not all API functions are supported over the Python wrappers. This example shows how to get a unique integer identifier of an AST, which can be used as a key in a hash-table.

Idea of the Algorithm​

The main idea of the algorithm is to maintain two logical contexts and exchange information between them:

  • The MapSolver is used to enumerate sets of clauses that are not already supersets of an existing unsatisfiable core and not already a subset of a maximal satisfying assignment. The MapSolver uses one unique atomic predicate per soft clause, so it enumerates sets of atomic predicates. For each minimal unsatisfiable core, say, represented by predicates

    p1, p2, p5, the MapSolver contains the clause ¬ p1 ∨ ¬ p2 ∨ ¬ p5. For each maximal satisfiable subset, say, represented by predicatsp2, p3, p5, theMapSolver contains a clause corresponding to the disjunction of all literals not in the maximal satisfiable subset, p1 ∨ p4 ∨ p6.

  • The SubsetSolver contains a set of soft clauses (clauses with the unique indicator atom occurring negated). The MapSolver feeds it a set of clauses (the indicator atoms). Recall that these are not already a superset of an existing minimal unsatisfiable core, or a subset of a maximal satisfying assignment. If asserting these atoms makes the SubsetSolver context infeasible, then it finds a minimal unsatisfiable subset corresponding to these atoms. If asserting the atoms is consistent with the SubsetSolver, then it extends this set of atoms maximally to a satisfying set.